M1, M2:MsgA.
M1  M2  (k:Knd, l:IdLnk, tg:Id. M2.sframe(k sends <l,tg>)  M1.sframe(k sends <l,tg>)) 

latex

Definitions	A & B, P  Q, x:A. B(x), f  g, f(x), Knd, KindDeq, t  T, True, T, EqDecider(T), deq-member(eq;x;L), Prop, , b, Id, IdLnk, x. t(x), a:A fp B(a), IdDeq, IdLnkDeq, product-deq(A;B;a;b), x  dom(f), z != f(x)  P(a;z), P & Q, Valtype(da;k), MsgA, M1  M2, M.sframe(k sends <l,tg>)
Lemmas	ma-sframe wf, ma-sub wf, msga wf, fpf-dom wf, IdLnk wf, Id wf, product-deq wf, idlnk-deq wf, id-deq wf, fpf-trivial-subtype-top, assert wf, bool wf, deq-member wf, squash wf, true wf, deq wf, Knd wf, Kind-deq wf